Nonnegative over a variety¶

The polynomial $1 - y^2$ is nonnegative for all $y$ in the unit circle. This can be verified using Sum-of-Squares.

In [1]:

using DynamicPolynomials
using SumOfSquares
@polyvar x y
S = @set x^2 + y^2 == 1

Out[1]:

Algebraic Set defined by 1 equalitty
 -1//1 + y^2 + x^2 = 0

We need to pick an SDP solver, see here for a list of the available choices. The domain over which the nonnegativity of $1 - y^2$ should be certified is specified through the domain keyword argument.

In [2]:

import CSDP
model = SOSModel(CSDP.Optimizer)
set_silent(model)
con_ref = @constraint(model, 1 - y^2 >= 0, domain = S)
optimize!(model)

We can see that the model was feasible:

In [3]:

solution_summary(model)

Out[3]:

* Solver : CSDP

* Status
  Result count       : 1
  Termination status : OPTIMAL
  Message from the solver:
  "Problem solved to optimality."

* Candidate solution (result #1)
  Primal status      : FEASIBLE_POINT
  Dual status        : FEASIBLE_POINT
  Objective value    : 0.00000e+00
  Dual objective value : 0.00000e+00

* Work counters
  Solve time (sec)   : 3.19009e-02

The certificate can be obtained as follows:

In [4]:

sos_decomposition(con_ref, 1e-6)

Out[4]:

(1.0000000044294615·x)^2

It returns $x^2$ which is a valid certificate as:

$1 - y^2 \equiv x^2 \pmod{x^2 + y^2 - 1}$

This notebook was generated using Literate.jl.